l:IdLnk, k:Knd, dt1, dt2:tg:Id fp Type.
k  dom(lnk-decl(l;dt1  dt2)) ~ (k  dom(lnk-decl(l;dt1)) k  dom(lnk-decl(l;dt2))) 

latex

Definitions

b, x  dom(f), lnk-decl(l;dt), x:A. B(x), t  T, x. t(x), Knd, Type, a:A fp B(a), Top, x:AB(x), p q, x.A(x), IdDeq, Id, f  g, KindDeq, P  Q, <a, b>, , s = t, {T}, SQType(T), s ~ t, IdLnk, x:A  B(x), left + right, type List, a < b, (x  l), False, A, x:A. B(x), P  Q, A c B, P & Q, Dec(P), map(f;as), Void, P  Q, P  Q, b, f(a), {x:A| B(x)} , mapfilter(f;P;L), , rcv(l,tg), Atom$n

Lemmas

member map, rcv wf, assert of bor, map append sq, member append, member map filter, l member wf, mapfilter wf, assert wf, iff functionality wrt iff, or functionality wrt iff, exists functionality wrt iff, and functionality wrt iff, cand functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, IdLnk wf, l member subtype, decidable l member, decidable equal Kind, bool sq, Id wf, iff imp equal bool, Kind-deq wf, fpf-join wf, id-deq wf, Knd wf, fpf wf, bor wf, fpf-dom wf, fpf-trivial-subtype-top, lnk-decl wf